Nuprl Lemma : kind_wf
11,40
postcript
pdf
E
:Type,
info
:(
E
((
:Id
Id) + (
:(
:IdLnk
E
)
Id))),
e
:
E
. kind(
e
)
Knd
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
kind(
e
)
,
x
.
t
(
x
)
,
x
(
s
)
Lemmas
locl
wf
,
pi2
wf
,
Id
wf
,
rcv
wf
,
pi1
wf
,
IdLnk
wf
origin
E:Type, info:(E
((:Id 
Id) + (:(:IdLnk E) Id))), e:E. kind(e) 
Knd E:Type, info:(E((:Id Id) + (:(:IdLnk E) Id))), e:E. kind(e) Knd x:A. B(x) T
x. t(x)